$\forall$$M$:MsgA, $x$:Id, $v$:$M$.ds($x$). $M$.init($x$)?$v$ $\in$ $M$.ds($x$)